$\forall$$T$:Type, $L$:$T$ List, $R$:($\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$$\rightarrow$Prop), $P$:($\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$$\rightarrow$Prop).
\\[0ex]Refl($\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$;$1$,$2$.$R$($1$,$2$)) $\Rightarrow$ causal\_order($L$;$R$;$P$;$P$)